Nuprl Lemma : dsys-compatible-join2
0,22
postcript
pdf
A
,
B
,
C
:Dsys.
A
||
B
A
||
C
B
||
C
A
B
||
C
latex
Definitions
t
T
,
f
(
a
)
,
P
Q
,
x
:
A
.
B
(
x
)
,
A
B
,
Id
,
x
:
A
B
(
x
)
,
A
||+
B
,
A
||
B
,
MsgA
,
Type
,
Dsys
Lemmas
m-sys-compatible
wf
,
msga
wf
,
Id
wf
,
ma-compat-join2
origin
A, B, C:Dsys. A || B 
A || C B || C A 
B || C A, B, C:Dsys. A || B A || C B || C A B || C 
T Qx:A. B(x) B
B(x)